(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(a,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

lessA(s(X1), s(X2)) :- lessA(X1, X2).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
pD(X1, X2, X3) :- lessF(X1, X2).
pD(X1, X2, X3) :- ','(lesscF(X1, X2), deleteB(X2, void, X3)).
delminG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delminG(X2, X4, X5).
pC(X1, X2, X3) :- lessA(X1, X2).
pC(X1, X2, X3) :- ','(lesscA(X1, X2), deleteE(X1, X3)).
pH(X1, X2, X3, X4) :- lessF(X1, X2).
pH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
lessM(s(X1), s(X2)) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X1, X3, X4)).
deleteK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delminG(X3, X4, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pI(X1, X2, X3, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
pJ(X1, X2, X3, X4) :- lessM(X1, X2).
pJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X2, X3, X4)).
pL(X1, X2, X3, X4) :- lessF(X1, X2).
pL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
deleteB(X1, tree(X2, void, void), tree(X2, X3, void)) :- pC(X1, X2, X3).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(0, tree(s(X1), void, void), tree(s(X1), X2, void)) :- deleteE(0, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- ','(lesscA(X1, X2), deleteE(s(X1), X3)).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deleteB(s(X1), void, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X3)).
deleteB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delminG(X3, X5, X6).
deleteB(X1, tree(X2, void, X3), tree(X2, X4, X3)) :- pC(X1, X2, X4).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(0, tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- deleteE(0, X3).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- ','(lesscA(X1, X2), deleteE(s(X1), X4)).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deleteB(s(X1), X2, X3).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X4, void)) :- lessA(X1, X2).
deleteB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delminG(X4, X5, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), pI(X1, X3, X4, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), pJ(X3, X1, X5, X6)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deleteK(0, X2, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deleteB(s(X1), void, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X4)).
deleteB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminG(X4, X6, X7).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- lessA(X1, X2).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deleteK(X1, X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteK(0, X2, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteB(s(X1), X3, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deleteB(s(X1), X4, X5)).

Clauses:

lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
deletecB(X1, tree(X1, void, X2), X2).
deletecB(X1, tree(X1, void, void), void).
deletecB(X1, tree(X2, void, void), tree(X2, X3, void)) :- qcC(X1, X2, X3).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(0, tree(s(X1), void, void), tree(s(X1), X2, void)) :- deletecE(0, X2).
deletecB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- ','(lesscA(X1, X2), deletecE(s(X1), X3)).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deletecB(s(X1), void, X2).
deletecB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X3)).
deletecB(X1, tree(X1, void, tree(X2, void, X3)), tree(X2, void, X3)).
deletecB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delmincG(X3, X5, X6).
deletecB(X1, tree(X2, void, X3), tree(X2, X4, X3)) :- qcC(X1, X2, X4).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(0, tree(s(X1), void, X2), tree(s(X1), X3, X2)) :- deletecE(0, X3).
deletecB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- ','(lesscA(X1, X2), deletecE(s(X1), X4)).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deletecB(s(X1), X2, X3).
deletecB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), X3, X4)).
deletecB(X1, tree(X1, X2, void), X2).
deletecB(X1, tree(X2, tree(X1, void, X3), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, void), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delmincG(X4, X5, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), qcI(X1, X3, X4, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), qcJ(X3, X1, X5, X6)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deletecK(0, X2, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X4)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deletecB(s(X1), void, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X4)).
deletecB(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincG(X4, X6, X7).
deletecB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deletecK(X1, X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecK(0, X2, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecB(s(X1), X3, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deletecB(s(X1), X4, X5)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
qcD(X1, X2, X3) :- ','(lesscF(X1, X2), deletecB(X2, void, X3)).
delmincG(tree(X1, void, X2), X1, X2).
delmincG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delmincG(X2, X4, X5).
qcC(X1, X2, X3) :- ','(lesscA(X1, X2), deletecE(X1, X3)).
qcH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).
lesscM(0, s(X1)).
lesscM(s(X1), s(X2)) :- lesscM(X1, X2).
qcI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X1, X3, X4)).
deletecK(X1, tree(X1, void, X2), X2).
deletecK(X1, tree(X1, X2, void), X2).
deletecK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delmincG(X3, X4, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcI(X1, X2, X3, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
qcJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X2, X3, X4)).
qcL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).

Afs:

deleteB(x1, x2, x3)  =  deleteB(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

lessA(s(X1), s(X2)) :- lessA(X1, X2).
lessF(s(X1), s(X2)) :- lessF(X1, X2).
pD(X1, X2, X3) :- lessF(X1, X2).
pD(X1, X2, X3) :- ','(lesscF(X1, X2), deleteB(X2, void, X3)).
delminG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delminG(X2, X4, X5).
pC(X1, X2, X3) :- lessA(X1, X2).
pH(X1, X2, X3, X4) :- lessF(X1, X2).
pH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
lessM(s(X1), s(X2)) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- lessM(X1, X2).
pI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X1, X3, X4)).
deleteK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delminG(X3, X4, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- pI(X1, X2, X3, X5).
deleteK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pJ(X2, X1, X4, X5).
pJ(X1, X2, X3, X4) :- lessM(X1, X2).
pJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deleteK(X2, X3, X4)).
pL(X1, X2, X3, X4) :- lessF(X1, X2).
pL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deleteB(X2, X3, X4)).
deleteB(X1, tree(X2, void, void), tree(X2, X3, void)) :- pC(X1, X2, X3).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) :- lessA(X1, X2).
deleteB(X1, tree(X2, void, void), tree(X2, void, X3)) :- pD(X2, X1, X3).
deleteB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deleteB(s(X1), void, X2).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X3)).
deleteB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delminG(X3, X5, X6).
deleteB(X1, tree(X2, void, X3), tree(X2, X4, X3)) :- pC(X1, X2, X4).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) :- lessA(X1, X2).
deleteB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- pH(X2, X1, X3, X4).
deleteB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deleteB(s(X1), X2, X3).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X4, void)) :- lessA(X1, X2).
deleteB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delminG(X4, X5, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), pI(X1, X3, X4, X6)).
deleteB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), pJ(X3, X1, X5, X6)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deleteK(0, X2, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X4)).
deleteB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- pD(X2, X1, X4).
deleteB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deleteB(s(X1), void, X3).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deleteB(s(X1), void, X4)).
deleteB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delminG(X4, X6, X7).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- lessA(X1, X2).
deleteB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deleteK(X1, X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deleteK(0, X2, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- lessA(X1, X2).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deleteK(s(X1), X3, X5)).
deleteB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- pL(X2, X1, X4, X5).
deleteB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deleteB(s(X1), X3, X4).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- lessF(X2, X1).
deleteB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deleteB(s(X1), X4, X5)).

Clauses:

lesscA(0, s(X1)).
lesscA(s(X1), s(X2)) :- lesscA(X1, X2).
deletecB(X1, tree(X1, void, X2), X2).
deletecB(X1, tree(X1, void, void), void).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(X1, tree(X2, void, void), tree(X2, void, X3)) :- qcD(X2, X1, X3).
deletecB(s(X1), tree(0, void, void), tree(0, void, X2)) :- deletecB(s(X1), void, X2).
deletecB(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X3)).
deletecB(X1, tree(X1, void, tree(X2, void, X3)), tree(X2, void, X3)).
deletecB(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) :- delmincG(X3, X5, X6).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(X1, tree(X2, void, X3), tree(X2, void, X4)) :- qcH(X2, X1, X3, X4).
deletecB(s(X1), tree(0, void, X2), tree(0, void, X3)) :- deletecB(s(X1), X2, X3).
deletecB(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), X3, X4)).
deletecB(X1, tree(X1, X2, void), X2).
deletecB(X1, tree(X2, tree(X1, void, X3), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, void), void), tree(X2, X3, void)) :- lesscA(X1, X2).
deletecB(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) :- ','(lesscA(X1, X2), delmincG(X4, X5, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) :- ','(lesscA(X1, X2), qcI(X1, X3, X4, X6)).
deletecB(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) :- ','(lesscA(X1, X2), qcJ(X3, X1, X5, X6)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) :- deletecK(0, X2, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X4)).
deletecB(X1, tree(X2, X3, void), tree(X2, X3, X4)) :- qcD(X2, X1, X4).
deletecB(s(X1), tree(0, X2, void), tree(0, X2, X3)) :- deletecB(s(X1), void, X3).
deletecB(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) :- ','(lesscF(X2, X1), deletecB(s(X1), void, X4)).
deletecB(X1, tree(X1, X2, tree(X3, void, X4)), tree(X3, X2, X4)).
deletecB(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) :- delmincG(X4, X6, X7).
deletecB(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- ','(lesscA(X1, X2), deletecK(X1, X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) :- deletecK(0, X2, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) :- ','(lesscA(X1, X2), deletecK(s(X1), X3, X5)).
deletecB(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcL(X2, X1, X4, X5).
deletecB(s(X1), tree(0, X2, X3), tree(0, X2, X4)) :- deletecB(s(X1), X3, X4).
deletecB(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) :- ','(lesscF(X2, X1), deletecB(s(X1), X4, X5)).
lesscF(0, s(X1)).
lesscF(s(X1), s(X2)) :- lesscF(X1, X2).
qcD(X1, X2, X3) :- ','(lesscF(X1, X2), deletecB(X2, void, X3)).
delmincG(tree(X1, void, X2), X1, X2).
delmincG(tree(X1, X2, X3), X4, tree(X1, X5, X6)) :- delmincG(X2, X4, X5).
qcH(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).
lesscM(0, s(X1)).
lesscM(s(X1), s(X2)) :- lesscM(X1, X2).
qcI(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X1, X3, X4)).
deletecK(X1, tree(X1, void, X2), X2).
deletecK(X1, tree(X1, X2, void), X2).
deletecK(X1, tree(X1, X2, X3), tree(X4, X2, X5)) :- delmincG(X3, X4, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X5, X4)) :- qcI(X1, X2, X3, X5).
deletecK(X1, tree(X2, X3, X4), tree(X2, X3, X5)) :- qcJ(X2, X1, X4, X5).
qcJ(X1, X2, X3, X4) :- ','(lesscM(X1, X2), deletecK(X2, X3, X4)).
qcL(X1, X2, X3, X4) :- ','(lesscF(X1, X2), deletecB(X2, X3, X4)).

Afs:

deleteB(x1, x2, x3)  =  deleteB(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
deleteB_in: (f,b,f)
pC_in: (f,b,f)
lessA_in: (f,b)
pD_in: (b,f,f)
lessF_in: (b,f)
lesscF_in: (b,f)
delminG_in: (b,f,f)
pH_in: (b,f,b,f)
lesscA_in: (b,b) (f,b)
pI_in: (b,b,b,f)
lessM_in: (b,b)
lesscM_in: (b,b)
deleteK_in: (b,b,f)
pJ_in: (b,b,b,f)
pL_in: (b,f,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → U24_AGA(X1, X2, X3, pC_in_aga(X1, X2, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → PC_IN_AGA(X1, X2, X3)
PC_IN_AGA(X1, X2, X3) → U7_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
PC_IN_AGA(X1, X2, X3) → LESSA_IN_AG(X1, X2)
LESSA_IN_AG(s(X1), s(X2)) → U1_AG(X1, X2, lessA_in_ag(X1, X2))
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → U25_AGA(X1, X2, X3, pD_in_gaa(X2, X1, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → PD_IN_GAA(X2, X1, X3)
PD_IN_GAA(X1, X2, X3) → U3_GAA(X1, X2, X3, lessF_in_ga(X1, X2))
PD_IN_GAA(X1, X2, X3) → LESSF_IN_GA(X1, X2)
LESSF_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, lessF_in_ga(X1, X2))
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
PD_IN_GAA(X1, X2, X3) → U4_GAA(X1, X2, X3, lesscF_in_ga(X1, X2))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → U5_GAA(X1, X2, X3, deleteB_in_aga(X2, void, X3))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → U26_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → U27_AGA(X1, X2, deleteB_in_aga(s(X1), void, X2))
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → DELETEB_IN_AGA(s(X1), void, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U28_AGA(X1, X2, X3, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U29_AGA(X1, X2, X3, lesscF_in_ga(X2, X1))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → U30_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → U31_AGA(X1, X2, X3, X4, X5, X6, X7, delminG_in_gaa(X3, X5, X6))
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → DELMING_IN_GAA(X3, X5, X6)
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U6_GAA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X2, X4, X5))
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → U32_AGA(X1, X2, X3, X4, pC_in_aga(X1, X2, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → PC_IN_AGA(X1, X2, X4)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → U33_AGA(X1, X2, X3, X4, pH_in_gaga(X2, X1, X3, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U8_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PH_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U10_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → U34_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → U35_AGA(X1, X2, X3, deleteB_in_aga(s(X1), X2, X3))
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U36_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U38_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → U39_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) → U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_gg(X1, X2))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → U41_AGA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X4, X5, X6))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → DELMING_IN_GAA(X4, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) → U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U43_AGA(X1, X2, X3, X4, X5, X6, pI_in_ggga(X1, X3, X4, X6))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PI_IN_GGGA(X1, X3, X4, X6)
PI_IN_GGGA(X1, X2, X3, X4) → U12_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PI_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
LESSM_IN_GG(s(X1), s(X2)) → U11_GG(X1, X2, lessM_in_gg(X1, X2))
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U14_GGGA(X1, X2, X3, X4, deleteK_in_gga(X1, X3, X4))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → U15_GGA(X1, X2, X3, X4, X5, delminG_in_gaa(X3, X4, X5))
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → DELMING_IN_GAA(X3, X4, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U16_GGA(X1, X2, X3, X4, X5, pI_in_ggga(X1, X2, X3, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U17_GGA(X1, X2, X3, X4, X5, pJ_in_ggga(X2, X1, X4, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U18_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PJ_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U20_GGGA(X1, X2, X3, X4, deleteK_in_gga(X2, X3, X4))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) → U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U45_AGA(X1, X2, X3, X4, X5, X6, pJ_in_ggga(X3, X1, X5, X6))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PJ_IN_GGGA(X3, X1, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → U46_AGA(X1, X2, X3, X4, pD_in_gaa(X2, X1, X4))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → PD_IN_GAA(X2, X1, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → U47_AGA(X1, X2, X3, deleteK_in_gga(0, X2, X3))
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → DELETEK_IN_GGA(0, X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U48_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U49_AGA(X1, X2, X3, X4, lesscA_in_ag(X1, X2))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → U50_AGA(X1, X2, X3, X4, deleteK_in_gga(s(X1), X3, X4))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → U51_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U52_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U53_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U54_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), void, X4))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X4)
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U55_AGA(X1, X2, X3, X4, X5, X6, X7, X8, delminG_in_gaa(X4, X6, X7))
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMING_IN_GAA(X4, X6, X7)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U56_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U57_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U58_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(X1, X3, X5))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(X1, X3, X5)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U59_AGA(X1, X2, X3, X4, X5, pL_in_gaga(X2, X1, X4, X5))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U21_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PL_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U23_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U60_AGA(X1, X2, X3, X4, deleteK_in_gga(0, X2, X4))
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEK_IN_GGA(0, X2, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U61_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U62_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U63_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(s(X1), X3, X5))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X5)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U64_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U65_AGA(X1, X2, X3, X4, X5, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → U67_AGA(X1, X2, X3, X4, X5, deleteB_in_aga(s(X1), X4, X5))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
deleteB_in_aga(x1, x2, x3)  =  deleteB_in_aga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
pC_in_aga(x1, x2, x3)  =  pC_in_aga(x2)
lessA_in_ag(x1, x2)  =  lessA_in_ag(x2)
s(x1)  =  s(x1)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
lessF_in_ga(x1, x2)  =  lessF_in_ga(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
delminG_in_gaa(x1, x2, x3)  =  delminG_in_gaa(x1)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
pI_in_ggga(x1, x2, x3, x4)  =  pI_in_ggga(x1, x2, x3)
lessM_in_gg(x1, x2)  =  lessM_in_gg(x1, x2)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
deleteK_in_gga(x1, x2, x3)  =  deleteK_in_gga(x1, x2)
pJ_in_ggga(x1, x2, x3, x4)  =  pJ_in_ggga(x1, x2, x3)
pL_in_gaga(x1, x2, x3, x4)  =  pL_in_gaga(x1, x3)
DELETEB_IN_AGA(x1, x2, x3)  =  DELETEB_IN_AGA(x2)
U24_AGA(x1, x2, x3, x4)  =  U24_AGA(x2, x4)
PC_IN_AGA(x1, x2, x3)  =  PC_IN_AGA(x2)
U7_AGA(x1, x2, x3, x4)  =  U7_AGA(x2, x4)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U25_AGA(x1, x2, x3, x4)  =  U25_AGA(x2, x4)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U26_AGA(x1, x2, x3, x4)  =  U26_AGA(x2, x4)
U27_AGA(x1, x2, x3)  =  U27_AGA(x3)
U28_AGA(x1, x2, x3, x4)  =  U28_AGA(x2, x4)
U29_AGA(x1, x2, x3, x4)  =  U29_AGA(x2, x4)
U30_AGA(x1, x2, x3, x4)  =  U30_AGA(x2, x4)
U31_AGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U31_AGA(x1, x2, x3, x4, x8)
DELMING_IN_GAA(x1, x2, x3)  =  DELMING_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x1, x2, x3, x7)
U32_AGA(x1, x2, x3, x4, x5)  =  U32_AGA(x2, x3, x5)
U33_AGA(x1, x2, x3, x4, x5)  =  U33_AGA(x2, x3, x5)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U8_GAGA(x1, x2, x3, x4, x5)  =  U8_GAGA(x1, x3, x5)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x3, x5)
U34_AGA(x1, x2, x3, x4, x5)  =  U34_AGA(x2, x3, x5)
U35_AGA(x1, x2, x3, x4)  =  U35_AGA(x2, x4)
U36_AGA(x1, x2, x3, x4, x5)  =  U36_AGA(x2, x3, x5)
U37_AGA(x1, x2, x3, x4, x5)  =  U37_AGA(x2, x3, x5)
U38_AGA(x1, x2, x3, x4, x5)  =  U38_AGA(x2, x3, x5)
U39_AGA(x1, x2, x3, x4, x5)  =  U39_AGA(x2, x3, x5)
U40_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U40_AGA(x1, x2, x3, x4, x7)
U41_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U41_AGA(x1, x2, x3, x4, x7)
U42_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U42_AGA(x2, x3, x4, x5, x7)
U43_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U43_AGA(x1, x2, x3, x4, x5, x7)
PI_IN_GGGA(x1, x2, x3, x4)  =  PI_IN_GGGA(x1, x2, x3)
U12_GGGA(x1, x2, x3, x4, x5)  =  U12_GGGA(x1, x2, x3, x5)
LESSM_IN_GG(x1, x2)  =  LESSM_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5)  =  U13_GGGA(x1, x2, x3, x5)
U14_GGGA(x1, x2, x3, x4, x5)  =  U14_GGGA(x1, x2, x3, x5)
DELETEK_IN_GGA(x1, x2, x3)  =  DELETEK_IN_GGA(x1, x2)
U15_GGA(x1, x2, x3, x4, x5, x6)  =  U15_GGA(x1, x2, x3, x6)
U16_GGA(x1, x2, x3, x4, x5, x6)  =  U16_GGA(x1, x2, x3, x4, x6)
U17_GGA(x1, x2, x3, x4, x5, x6)  =  U17_GGA(x1, x2, x3, x4, x6)
PJ_IN_GGGA(x1, x2, x3, x4)  =  PJ_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4, x5)  =  U18_GGGA(x1, x2, x3, x5)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x1, x2, x3, x5)
U20_GGGA(x1, x2, x3, x4, x5)  =  U20_GGGA(x1, x2, x3, x5)
U44_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U44_AGA(x2, x3, x4, x5, x7)
U45_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U45_AGA(x1, x2, x3, x4, x5, x7)
U46_AGA(x1, x2, x3, x4, x5)  =  U46_AGA(x2, x3, x5)
U47_AGA(x1, x2, x3, x4)  =  U47_AGA(x1, x2, x4)
U48_AGA(x1, x2, x3, x4, x5)  =  U48_AGA(x2, x3, x5)
U49_AGA(x1, x2, x3, x4, x5)  =  U49_AGA(x2, x3, x5)
U50_AGA(x1, x2, x3, x4, x5)  =  U50_AGA(x1, x2, x3, x5)
U51_AGA(x1, x2, x3, x4)  =  U51_AGA(x2, x4)
U52_AGA(x1, x2, x3, x4, x5)  =  U52_AGA(x2, x3, x5)
U53_AGA(x1, x2, x3, x4, x5)  =  U53_AGA(x2, x3, x5)
U54_AGA(x1, x2, x3, x4, x5)  =  U54_AGA(x2, x3, x5)
U55_AGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_AGA(x1, x2, x3, x4, x5, x9)
U56_AGA(x1, x2, x3, x4, x5, x6)  =  U56_AGA(x2, x3, x4, x6)
U57_AGA(x1, x2, x3, x4, x5, x6)  =  U57_AGA(x2, x3, x4, x6)
U58_AGA(x1, x2, x3, x4, x5, x6)  =  U58_AGA(x1, x2, x3, x4, x6)
U59_AGA(x1, x2, x3, x4, x5, x6)  =  U59_AGA(x2, x3, x4, x6)
PL_IN_GAGA(x1, x2, x3, x4)  =  PL_IN_GAGA(x1, x3)
U21_GAGA(x1, x2, x3, x4, x5)  =  U21_GAGA(x1, x3, x5)
U22_GAGA(x1, x2, x3, x4, x5)  =  U22_GAGA(x1, x3, x5)
U23_GAGA(x1, x2, x3, x4, x5)  =  U23_GAGA(x1, x3, x5)
U60_AGA(x1, x2, x3, x4, x5)  =  U60_AGA(x1, x2, x3, x5)
U61_AGA(x1, x2, x3, x4, x5, x6)  =  U61_AGA(x2, x3, x4, x6)
U62_AGA(x1, x2, x3, x4, x5, x6)  =  U62_AGA(x2, x3, x4, x6)
U63_AGA(x1, x2, x3, x4, x5, x6)  =  U63_AGA(x1, x2, x3, x4, x6)
U64_AGA(x1, x2, x3, x4, x5)  =  U64_AGA(x2, x3, x5)
U65_AGA(x1, x2, x3, x4, x5, x6)  =  U65_AGA(x2, x3, x4, x6)
U66_AGA(x1, x2, x3, x4, x5, x6)  =  U66_AGA(x2, x3, x4, x6)
U67_AGA(x1, x2, x3, x4, x5, x6)  =  U67_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → U24_AGA(X1, X2, X3, pC_in_aga(X1, X2, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, X3, void)) → PC_IN_AGA(X1, X2, X3)
PC_IN_AGA(X1, X2, X3) → U7_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
PC_IN_AGA(X1, X2, X3) → LESSA_IN_AG(X1, X2)
LESSA_IN_AG(s(X1), s(X2)) → U1_AG(X1, X2, lessA_in_ag(X1, X2))
LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → U25_AGA(X1, X2, X3, pD_in_gaa(X2, X1, X3))
DELETEB_IN_AGA(X1, tree(X2, void, void), tree(X2, void, X3)) → PD_IN_GAA(X2, X1, X3)
PD_IN_GAA(X1, X2, X3) → U3_GAA(X1, X2, X3, lessF_in_ga(X1, X2))
PD_IN_GAA(X1, X2, X3) → LESSF_IN_GA(X1, X2)
LESSF_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, lessF_in_ga(X1, X2))
LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)
PD_IN_GAA(X1, X2, X3) → U4_GAA(X1, X2, X3, lesscF_in_ga(X1, X2))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → U5_GAA(X1, X2, X3, deleteB_in_aga(X2, void, X3))
U4_GAA(X1, X2, X3, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → U26_AGA(X1, X2, X3, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), X3, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → U27_AGA(X1, X2, deleteB_in_aga(s(X1), void, X2))
DELETEB_IN_AGA(s(X1), tree(0, void, void), tree(0, void, X2)) → DELETEB_IN_AGA(s(X1), void, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U28_AGA(X1, X2, X3, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, void), tree(s(X2), void, X3)) → U29_AGA(X1, X2, X3, lesscF_in_ga(X2, X1))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → U30_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
U29_AGA(X1, X2, X3, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → U31_AGA(X1, X2, X3, X4, X5, X6, X7, delminG_in_gaa(X3, X5, X6))
DELETEB_IN_AGA(X1, tree(X1, void, tree(X2, X3, X4)), tree(X5, void, tree(X2, X6, X7))) → DELMING_IN_GAA(X3, X5, X6)
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → U6_GAA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X2, X4, X5))
DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → U32_AGA(X1, X2, X3, X4, pC_in_aga(X1, X2, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, X4, X3)) → PC_IN_AGA(X1, X2, X4)
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → U33_AGA(X1, X2, X3, X4, pH_in_gaga(X2, X1, X3, X4))
DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U8_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PH_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U10_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → U34_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), X4, X3)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → U35_AGA(X1, X2, X3, deleteB_in_aga(s(X1), X2, X3))
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U36_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U38_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → U39_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, tree(X1, X3, X4), void), tree(X2, tree(X5, X3, X6), void)) → U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_gg(X1, X2))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → U41_AGA(X1, X2, X3, X4, X5, X6, delminG_in_gaa(X4, X5, X6))
U40_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_gg(X1, X2)) → DELMING_IN_GAA(X4, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X6, X5), void)) → U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U43_AGA(X1, X2, X3, X4, X5, X6, pI_in_ggga(X1, X3, X4, X6))
U42_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PI_IN_GGGA(X1, X3, X4, X6)
PI_IN_GGGA(X1, X2, X3, X4) → U12_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PI_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
LESSM_IN_GG(s(X1), s(X2)) → U11_GG(X1, X2, lessM_in_gg(X1, X2))
LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U14_GGGA(X1, X2, X3, X4, deleteK_in_gga(X1, X3, X4))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → U15_GGA(X1, X2, X3, X4, X5, delminG_in_gaa(X3, X4, X5))
DELETEK_IN_GGA(X1, tree(X1, X2, X3), tree(X4, X2, X5)) → DELMING_IN_GAA(X3, X4, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U16_GGA(X1, X2, X3, X4, X5, pI_in_ggga(X1, X2, X3, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U17_GGA(X1, X2, X3, X4, X5, pJ_in_ggga(X2, X1, X4, X5))
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U18_GGGA(X1, X2, X3, X4, lessM_in_gg(X1, X2))
PJ_IN_GGGA(X1, X2, X3, X4) → LESSM_IN_GG(X1, X2)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → U20_GGGA(X1, X2, X3, X4, deleteK_in_gga(X2, X3, X4))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)
DELETEB_IN_AGA(X1, tree(X2, tree(X3, X4, X5), void), tree(X2, tree(X3, X4, X6), void)) → U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_in_ag(X1, X2))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → U45_AGA(X1, X2, X3, X4, X5, X6, pJ_in_ggga(X3, X1, X5, X6))
U44_AGA(X1, X2, X3, X4, X5, X6, lesscA_out_ag(X1, X2)) → PJ_IN_GGGA(X3, X1, X5, X6)
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → U46_AGA(X1, X2, X3, X4, pD_in_gaa(X2, X1, X4))
DELETEB_IN_AGA(X1, tree(X2, X3, void), tree(X2, X3, X4)) → PD_IN_GAA(X2, X1, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → U47_AGA(X1, X2, X3, deleteK_in_gga(0, X2, X3))
DELETEB_IN_AGA(0, tree(s(X1), X2, void), tree(s(X1), X3, void)) → DELETEK_IN_GGA(0, X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U48_AGA(X1, X2, X3, X4, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X4, void)) → U49_AGA(X1, X2, X3, X4, lesscA_in_ag(X1, X2))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → U50_AGA(X1, X2, X3, X4, deleteK_in_gga(s(X1), X3, X4))
U49_AGA(X1, X2, X3, X4, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → U51_AGA(X1, X2, X3, deleteB_in_aga(s(X1), void, X3))
DELETEB_IN_AGA(s(X1), tree(0, X2, void), tree(0, X2, X3)) → DELETEB_IN_AGA(s(X1), void, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U52_AGA(X1, X2, X3, X4, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, void), tree(s(X2), X3, X4)) → U53_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → U54_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), void, X4))
U53_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), void, X4)
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → U55_AGA(X1, X2, X3, X4, X5, X6, X7, X8, delminG_in_gaa(X4, X6, X7))
DELETEB_IN_AGA(X1, tree(X1, X2, tree(X3, X4, X5)), tree(X6, X2, tree(X3, X7, X8))) → DELMING_IN_GAA(X4, X6, X7)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U56_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → U57_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U58_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(X1, X3, X5))
U57_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(X1, X3, X5)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → U59_AGA(X1, X2, X3, X4, X5, pL_in_gaga(X2, X1, X4, X5))
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U21_GAGA(X1, X2, X3, X4, lessF_in_ga(X1, X2))
PL_IN_GAGA(X1, X2, X3, X4) → LESSF_IN_GA(X1, X2)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → U23_GAGA(X1, X2, X3, X4, deleteB_in_aga(X2, X3, X4))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → U60_AGA(X1, X2, X3, X4, deleteK_in_gga(0, X2, X4))
DELETEB_IN_AGA(0, tree(s(X1), X2, X3), tree(s(X1), X4, X3)) → DELETEK_IN_GGA(0, X2, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U61_AGA(X1, X2, X3, X4, X5, lessA_in_ag(X1, X2))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → LESSA_IN_AG(X1, X2)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X5, X4)) → U62_AGA(X1, X2, X3, X4, X5, lesscA_in_ag(X1, X2))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → U63_AGA(X1, X2, X3, X4, X5, deleteK_in_gga(s(X1), X3, X5))
U62_AGA(X1, X2, X3, X4, X5, lesscA_out_ag(X1, X2)) → DELETEK_IN_GGA(s(X1), X3, X5)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → U64_AGA(X1, X2, X3, X4, deleteB_in_aga(s(X1), X3, X4))
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U65_AGA(X1, X2, X3, X4, X5, lessF_in_ga(X2, X1))
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → LESSF_IN_GA(X2, X1)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → U67_AGA(X1, X2, X3, X4, X5, deleteB_in_aga(s(X1), X4, X5))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
deleteB_in_aga(x1, x2, x3)  =  deleteB_in_aga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
pC_in_aga(x1, x2, x3)  =  pC_in_aga(x2)
lessA_in_ag(x1, x2)  =  lessA_in_ag(x2)
s(x1)  =  s(x1)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
lessF_in_ga(x1, x2)  =  lessF_in_ga(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
delminG_in_gaa(x1, x2, x3)  =  delminG_in_gaa(x1)
pH_in_gaga(x1, x2, x3, x4)  =  pH_in_gaga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
pI_in_ggga(x1, x2, x3, x4)  =  pI_in_ggga(x1, x2, x3)
lessM_in_gg(x1, x2)  =  lessM_in_gg(x1, x2)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
deleteK_in_gga(x1, x2, x3)  =  deleteK_in_gga(x1, x2)
pJ_in_ggga(x1, x2, x3, x4)  =  pJ_in_ggga(x1, x2, x3)
pL_in_gaga(x1, x2, x3, x4)  =  pL_in_gaga(x1, x3)
DELETEB_IN_AGA(x1, x2, x3)  =  DELETEB_IN_AGA(x2)
U24_AGA(x1, x2, x3, x4)  =  U24_AGA(x2, x4)
PC_IN_AGA(x1, x2, x3)  =  PC_IN_AGA(x2)
U7_AGA(x1, x2, x3, x4)  =  U7_AGA(x2, x4)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U25_AGA(x1, x2, x3, x4)  =  U25_AGA(x2, x4)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U26_AGA(x1, x2, x3, x4)  =  U26_AGA(x2, x4)
U27_AGA(x1, x2, x3)  =  U27_AGA(x3)
U28_AGA(x1, x2, x3, x4)  =  U28_AGA(x2, x4)
U29_AGA(x1, x2, x3, x4)  =  U29_AGA(x2, x4)
U30_AGA(x1, x2, x3, x4)  =  U30_AGA(x2, x4)
U31_AGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U31_AGA(x1, x2, x3, x4, x8)
DELMING_IN_GAA(x1, x2, x3)  =  DELMING_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x1, x2, x3, x7)
U32_AGA(x1, x2, x3, x4, x5)  =  U32_AGA(x2, x3, x5)
U33_AGA(x1, x2, x3, x4, x5)  =  U33_AGA(x2, x3, x5)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U8_GAGA(x1, x2, x3, x4, x5)  =  U8_GAGA(x1, x3, x5)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x3, x5)
U34_AGA(x1, x2, x3, x4, x5)  =  U34_AGA(x2, x3, x5)
U35_AGA(x1, x2, x3, x4)  =  U35_AGA(x2, x4)
U36_AGA(x1, x2, x3, x4, x5)  =  U36_AGA(x2, x3, x5)
U37_AGA(x1, x2, x3, x4, x5)  =  U37_AGA(x2, x3, x5)
U38_AGA(x1, x2, x3, x4, x5)  =  U38_AGA(x2, x3, x5)
U39_AGA(x1, x2, x3, x4, x5)  =  U39_AGA(x2, x3, x5)
U40_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U40_AGA(x1, x2, x3, x4, x7)
U41_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U41_AGA(x1, x2, x3, x4, x7)
U42_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U42_AGA(x2, x3, x4, x5, x7)
U43_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U43_AGA(x1, x2, x3, x4, x5, x7)
PI_IN_GGGA(x1, x2, x3, x4)  =  PI_IN_GGGA(x1, x2, x3)
U12_GGGA(x1, x2, x3, x4, x5)  =  U12_GGGA(x1, x2, x3, x5)
LESSM_IN_GG(x1, x2)  =  LESSM_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5)  =  U13_GGGA(x1, x2, x3, x5)
U14_GGGA(x1, x2, x3, x4, x5)  =  U14_GGGA(x1, x2, x3, x5)
DELETEK_IN_GGA(x1, x2, x3)  =  DELETEK_IN_GGA(x1, x2)
U15_GGA(x1, x2, x3, x4, x5, x6)  =  U15_GGA(x1, x2, x3, x6)
U16_GGA(x1, x2, x3, x4, x5, x6)  =  U16_GGA(x1, x2, x3, x4, x6)
U17_GGA(x1, x2, x3, x4, x5, x6)  =  U17_GGA(x1, x2, x3, x4, x6)
PJ_IN_GGGA(x1, x2, x3, x4)  =  PJ_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4, x5)  =  U18_GGGA(x1, x2, x3, x5)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x1, x2, x3, x5)
U20_GGGA(x1, x2, x3, x4, x5)  =  U20_GGGA(x1, x2, x3, x5)
U44_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U44_AGA(x2, x3, x4, x5, x7)
U45_AGA(x1, x2, x3, x4, x5, x6, x7)  =  U45_AGA(x1, x2, x3, x4, x5, x7)
U46_AGA(x1, x2, x3, x4, x5)  =  U46_AGA(x2, x3, x5)
U47_AGA(x1, x2, x3, x4)  =  U47_AGA(x1, x2, x4)
U48_AGA(x1, x2, x3, x4, x5)  =  U48_AGA(x2, x3, x5)
U49_AGA(x1, x2, x3, x4, x5)  =  U49_AGA(x2, x3, x5)
U50_AGA(x1, x2, x3, x4, x5)  =  U50_AGA(x1, x2, x3, x5)
U51_AGA(x1, x2, x3, x4)  =  U51_AGA(x2, x4)
U52_AGA(x1, x2, x3, x4, x5)  =  U52_AGA(x2, x3, x5)
U53_AGA(x1, x2, x3, x4, x5)  =  U53_AGA(x2, x3, x5)
U54_AGA(x1, x2, x3, x4, x5)  =  U54_AGA(x2, x3, x5)
U55_AGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U55_AGA(x1, x2, x3, x4, x5, x9)
U56_AGA(x1, x2, x3, x4, x5, x6)  =  U56_AGA(x2, x3, x4, x6)
U57_AGA(x1, x2, x3, x4, x5, x6)  =  U57_AGA(x2, x3, x4, x6)
U58_AGA(x1, x2, x3, x4, x5, x6)  =  U58_AGA(x1, x2, x3, x4, x6)
U59_AGA(x1, x2, x3, x4, x5, x6)  =  U59_AGA(x2, x3, x4, x6)
PL_IN_GAGA(x1, x2, x3, x4)  =  PL_IN_GAGA(x1, x3)
U21_GAGA(x1, x2, x3, x4, x5)  =  U21_GAGA(x1, x3, x5)
U22_GAGA(x1, x2, x3, x4, x5)  =  U22_GAGA(x1, x3, x5)
U23_GAGA(x1, x2, x3, x4, x5)  =  U23_GAGA(x1, x3, x5)
U60_AGA(x1, x2, x3, x4, x5)  =  U60_AGA(x1, x2, x3, x5)
U61_AGA(x1, x2, x3, x4, x5, x6)  =  U61_AGA(x2, x3, x4, x6)
U62_AGA(x1, x2, x3, x4, x5, x6)  =  U62_AGA(x2, x3, x4, x6)
U63_AGA(x1, x2, x3, x4, x5, x6)  =  U63_AGA(x1, x2, x3, x4, x6)
U64_AGA(x1, x2, x3, x4, x5)  =  U64_AGA(x2, x3, x5)
U65_AGA(x1, x2, x3, x4, x5, x6)  =  U65_AGA(x2, x3, x4, x6)
U66_AGA(x1, x2, x3, x4, x5, x6)  =  U66_AGA(x2, x3, x4, x6)
U67_AGA(x1, x2, x3, x4, x5, x6)  =  U67_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 97 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
LESSM_IN_GG(x1, x2)  =  LESSM_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSM_IN_GG(s(X1), s(X2)) → LESSM_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
DELMING_IN_GAA(x1, x2, x3)  =  DELMING_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELMING_IN_GAA(tree(X1, X2, X3), X4, tree(X1, X5, X6)) → DELMING_IN_GAA(X2, X4, X5)

R is empty.
The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
DELMING_IN_GAA(x1, x2, x3)  =  DELMING_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELMING_IN_GAA(tree(X1, X2, X3)) → DELMING_IN_GAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • DELMING_IN_GAA(tree(X1, X2, X3)) → DELMING_IN_GAA(X2)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
PI_IN_GGGA(x1, x2, x3, x4)  =  PI_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5)  =  U13_GGGA(x1, x2, x3, x5)
DELETEK_IN_GGA(x1, x2, x3)  =  DELETEK_IN_GGA(x1, x2)
PJ_IN_GGGA(x1, x2, x3, x4)  =  PJ_IN_GGGA(x1, x2, x3)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X5, X4)) → PI_IN_GGGA(X1, X2, X3, X5)
PI_IN_GGGA(X1, X2, X3, X4) → U13_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3, X4)
DELETEK_IN_GGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PJ_IN_GGGA(X2, X1, X4, X5)
PJ_IN_GGGA(X1, X2, X3, X4) → U19_GGGA(X1, X2, X3, X4, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, X4, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
PI_IN_GGGA(x1, x2, x3, x4)  =  PI_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5)  =  U13_GGGA(x1, x2, x3, x5)
DELETEK_IN_GGA(x1, x2, x3)  =  DELETEK_IN_GGA(x1, x2)
PJ_IN_GGGA(x1, x2, x3, x4)  =  PJ_IN_GGGA(x1, x2, x3)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PI_IN_GGGA(X1, X2, X3)
PI_IN_GGGA(X1, X2, X3) → U13_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
U13_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3)
DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PJ_IN_GGGA(X2, X1, X4)
PJ_IN_GGGA(X1, X2, X3) → U19_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
U19_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3)

The TRS R consists of the following rules:

lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

lesscM_in_gg(x0, x1)
U110_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PI_IN_GGGA(X1, X2, X3) → U13_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U13_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • U19_GGGA(X1, X2, X3, lesscM_out_gg(X1, X2)) → DELETEK_IN_GGA(X2, X3)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PI_IN_GGGA(X1, X2, X3)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • DELETEK_IN_GGA(X1, tree(X2, X3, X4)) → PJ_IN_GGGA(X2, X1, X4)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • PJ_IN_GGGA(X1, X2, X3) → U19_GGGA(X1, X2, X3, lesscM_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSF_IN_GA(s(X1), s(X2)) → LESSF_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSF_IN_GA(x1, x2)  =  LESSF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSF_IN_GA(s(X1)) → LESSF_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSF_IN_GA(s(X1)) → LESSF_IN_GA(X1)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LESSA_IN_AG(s(X1), s(X2)) → LESSA_IN_AG(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSA_IN_AG(x1, x2)  =  LESSA_IN_AG(x2)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LESSA_IN_AG(s(X2)) → LESSA_IN_AG(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LESSA_IN_AG(s(X2)) → LESSA_IN_AG(X2)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))
lesscA_in_gg(0, s(X1)) → lesscA_out_gg(0, s(X1))
lesscA_in_gg(s(X1), s(X2)) → U69_gg(X1, X2, lesscA_in_gg(X1, X2))
U69_gg(X1, X2, lesscA_out_gg(X1, X2)) → lesscA_out_gg(s(X1), s(X2))
lesscA_in_ag(0, s(X1)) → lesscA_out_ag(0, s(X1))
lesscA_in_ag(s(X1), s(X2)) → U69_ag(X1, X2, lesscA_in_ag(X1, X2))
U69_ag(X1, X2, lesscA_out_ag(X1, X2)) → lesscA_out_ag(s(X1), s(X2))
lesscM_in_gg(0, s(X1)) → lesscM_out_gg(0, s(X1))
lesscM_in_gg(s(X1), s(X2)) → U110_gg(X1, X2, lesscM_in_gg(X1, X2))
U110_gg(X1, X2, lesscM_out_gg(X1, X2)) → lesscM_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
lesscA_in_gg(x1, x2)  =  lesscA_in_gg(x1, x2)
lesscA_out_gg(x1, x2)  =  lesscA_out_gg(x1, x2)
U69_gg(x1, x2, x3)  =  U69_gg(x1, x2, x3)
lesscA_in_ag(x1, x2)  =  lesscA_in_ag(x2)
lesscA_out_ag(x1, x2)  =  lesscA_out_ag(x1, x2)
U69_ag(x1, x2, x3)  =  U69_ag(x2, x3)
lesscM_in_gg(x1, x2)  =  lesscM_in_gg(x1, x2)
lesscM_out_gg(x1, x2)  =  lesscM_out_gg(x1, x2)
U110_gg(x1, x2, x3)  =  U110_gg(x1, x2, x3)
DELETEB_IN_AGA(x1, x2, x3)  =  DELETEB_IN_AGA(x2)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U37_AGA(x1, x2, x3, x4, x5)  =  U37_AGA(x2, x3, x5)
PL_IN_GAGA(x1, x2, x3, x4)  =  PL_IN_GAGA(x1, x3)
U22_GAGA(x1, x2, x3, x4, x5)  =  U22_GAGA(x1, x3, x5)
U66_AGA(x1, x2, x3, x4, x5, x6)  =  U66_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DELETEB_IN_AGA(X1, tree(X2, void, X3), tree(X2, void, X4)) → PH_IN_GAGA(X2, X1, X3, X4)
PH_IN_GAGA(X1, X2, X3, X4) → U9_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U9_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, void, X2), tree(0, void, X3)) → DELETEB_IN_AGA(s(X1), X2, X3)
DELETEB_IN_AGA(s(X1), tree(s(X2), void, X3), tree(s(X2), void, X4)) → U37_AGA(X1, X2, X3, X4, lesscF_in_ga(X2, X1))
U37_AGA(X1, X2, X3, X4, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(X1, tree(X2, X3, X4), tree(X2, X3, X5)) → PL_IN_GAGA(X2, X1, X4, X5)
PL_IN_GAGA(X1, X2, X3, X4) → U22_GAGA(X1, X2, X3, X4, lesscF_in_ga(X1, X2))
U22_GAGA(X1, X2, X3, X4, lesscF_out_ga(X1, X2)) → DELETEB_IN_AGA(X2, X3, X4)
DELETEB_IN_AGA(s(X1), tree(0, X2, X3), tree(0, X2, X4)) → DELETEB_IN_AGA(s(X1), X3, X4)
DELETEB_IN_AGA(s(X1), tree(s(X2), X3, X4), tree(s(X2), X3, X5)) → U66_AGA(X1, X2, X3, X4, X5, lesscF_in_ga(X2, X1))
U66_AGA(X1, X2, X3, X4, X5, lesscF_out_ga(X2, X1)) → DELETEB_IN_AGA(s(X1), X4, X5)

The TRS R consists of the following rules:

lesscF_in_ga(0, s(X1)) → lesscF_out_ga(0, s(X1))
lesscF_in_ga(s(X1), s(X2)) → U104_ga(X1, X2, lesscF_in_ga(X1, X2))
U104_ga(X1, X2, lesscF_out_ga(X1, X2)) → lesscF_out_ga(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
s(x1)  =  s(x1)
lesscF_in_ga(x1, x2)  =  lesscF_in_ga(x1)
0  =  0
lesscF_out_ga(x1, x2)  =  lesscF_out_ga(x1)
U104_ga(x1, x2, x3)  =  U104_ga(x1, x3)
DELETEB_IN_AGA(x1, x2, x3)  =  DELETEB_IN_AGA(x2)
PH_IN_GAGA(x1, x2, x3, x4)  =  PH_IN_GAGA(x1, x3)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U37_AGA(x1, x2, x3, x4, x5)  =  U37_AGA(x2, x3, x5)
PL_IN_GAGA(x1, x2, x3, x4)  =  PL_IN_GAGA(x1, x3)
U22_GAGA(x1, x2, x3, x4, x5)  =  U22_GAGA(x1, x3, x5)
U66_AGA(x1, x2, x3, x4, x5, x6)  =  U66_AGA(x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DELETEB_IN_AGA(tree(X2, void, X3)) → PH_IN_GAGA(X2, X3)
PH_IN_GAGA(X1, X3) → U9_GAGA(X1, X3, lesscF_in_ga(X1))
U9_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(0, void, X2)) → DELETEB_IN_AGA(X2)
DELETEB_IN_AGA(tree(s(X2), void, X3)) → U37_AGA(X2, X3, lesscF_in_ga(X2))
U37_AGA(X2, X3, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(X2, X3, X4)) → PL_IN_GAGA(X2, X4)
PL_IN_GAGA(X1, X3) → U22_GAGA(X1, X3, lesscF_in_ga(X1))
U22_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(0, X2, X3)) → DELETEB_IN_AGA(X3)
DELETEB_IN_AGA(tree(s(X2), X3, X4)) → U66_AGA(X2, X3, X4, lesscF_in_ga(X2))
U66_AGA(X2, X3, X4, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X4)

The TRS R consists of the following rules:

lesscF_in_ga(0) → lesscF_out_ga(0)
lesscF_in_ga(s(X1)) → U104_ga(X1, lesscF_in_ga(X1))
U104_ga(X1, lesscF_out_ga(X1)) → lesscF_out_ga(s(X1))

The set Q consists of the following terms:

lesscF_in_ga(x0)
U104_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • PH_IN_GAGA(X1, X3) → U9_GAGA(X1, X3, lesscF_in_ga(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U9_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
    The graph contains the following edges 2 >= 1

  • DELETEB_IN_AGA(tree(X2, void, X3)) → PH_IN_GAGA(X2, X3)
    The graph contains the following edges 1 > 1, 1 > 2

  • PL_IN_GAGA(X1, X3) → U22_GAGA(X1, X3, lesscF_in_ga(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U37_AGA(X2, X3, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X3)
    The graph contains the following edges 2 >= 1

  • DELETEB_IN_AGA(tree(s(X2), void, X3)) → U37_AGA(X2, X3, lesscF_in_ga(X2))
    The graph contains the following edges 1 > 1, 1 > 2

  • U22_GAGA(X1, X3, lesscF_out_ga(X1)) → DELETEB_IN_AGA(X3)
    The graph contains the following edges 2 >= 1

  • U66_AGA(X2, X3, X4, lesscF_out_ga(X2)) → DELETEB_IN_AGA(X4)
    The graph contains the following edges 3 >= 1

  • DELETEB_IN_AGA(tree(X2, X3, X4)) → PL_IN_GAGA(X2, X4)
    The graph contains the following edges 1 > 1, 1 > 2

  • DELETEB_IN_AGA(tree(s(X2), X3, X4)) → U66_AGA(X2, X3, X4, lesscF_in_ga(X2))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

  • DELETEB_IN_AGA(tree(0, void, X2)) → DELETEB_IN_AGA(X2)
    The graph contains the following edges 1 > 1

  • DELETEB_IN_AGA(tree(0, X2, X3)) → DELETEB_IN_AGA(X3)
    The graph contains the following edges 1 > 1

(50) YES